(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, 1).
The TRS R consists of the following rules:
fst(0, Z) → nil
fst(s, cons(Y)) → cons(Y)
from(X) → cons(X)
add(0, X) → X
add(s, Y) → s
len(nil) → 0
len(cons(X)) → s
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
00() → 0
nil0() → 0
s0() → 0
cons0(0) → 0
fst0(0, 0) → 1
from0(0) → 2
add0(0, 0) → 3
len0(0) → 4
nil1() → 1
cons1(0) → 1
cons1(0) → 2
s1() → 3
01() → 4
s1() → 4
0 → 3
(2) BOUNDS(1, n^1)
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
fst(0, z0) → nil
fst(s, cons(z0)) → cons(z0)
from(z0) → cons(z0)
add(0, z0) → z0
add(s, z0) → s
len(nil) → 0
len(cons(z0)) → s
Tuples:
FST(0, z0) → c
FST(s, cons(z0)) → c1
FROM(z0) → c2
ADD(0, z0) → c3
ADD(s, z0) → c4
LEN(nil) → c5
LEN(cons(z0)) → c6
S tuples:
FST(0, z0) → c
FST(s, cons(z0)) → c1
FROM(z0) → c2
ADD(0, z0) → c3
ADD(s, z0) → c4
LEN(nil) → c5
LEN(cons(z0)) → c6
K tuples:none
Defined Rule Symbols:
fst, from, add, len
Defined Pair Symbols:
FST, FROM, ADD, LEN
Compound Symbols:
c, c1, c2, c3, c4, c5, c6
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 7 trailing nodes:
FST(0, z0) → c
LEN(nil) → c5
ADD(0, z0) → c3
FST(s, cons(z0)) → c1
FROM(z0) → c2
LEN(cons(z0)) → c6
ADD(s, z0) → c4
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
fst(0, z0) → nil
fst(s, cons(z0)) → cons(z0)
from(z0) → cons(z0)
add(0, z0) → z0
add(s, z0) → s
len(nil) → 0
len(cons(z0)) → s
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
fst, from, add, len
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(8) BOUNDS(1, 1)